Inference at * 2 1 1 
Iof proof for Lemma before-adjacent:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x, y:T.
5. no_repeats(T;v)  adjacent(T;v;x;y)  (z:T. z before y  v  (z before x  v  (z = x)))
6. x : T
7. y : T
8. no_repeats(T;[u / v])
9. 0 < ||v||
10. x = u & y = hd(v)
11. z : T
12. z before y  [u / v]
  ((z = u & (x  v))  z before x  v)  (z = x) 

latex

 by ((((RWO "cons_before" (-1)) 
CollapseTHENA (Auto))) 
CollapseTHEN (((D (-1)) 

CoCollapseTHEN (MaAuto)))) 

latex

C1: 

C1: 10. x = u
C1: 11. y = hd(v)
C1: 12. z : T
C1: 13. z = u
C1: 14. (y  v)
C1:   ((z = u & (x  v))  z before x  v)  (z = x)
C2: 

C2: 10. x = u
C2: 11. y = hd(v)
C2: 12. z : T
C2: 13. z before y  v
C2:   ((z = u & (x  v))  z before x  v)  (z = x)
C.

Definitions	hd(l), #$n, ||as||, [car / cdr], adjacent(T;L;x;y), no_repeats(T;l), L1  L2, type List, x:A.B(x), , Type, (x  l), x before y  l, Unit, (xL.P(x)), xL. P(x), |r|, x f y, f(a), A c B, a < b, |g|, a <p b, a  b, |p|, a ~ b, b | a, x:A. B(x), x,y:A//B(x;y), b, , {i..j}, Atom, A  B, a < b, , P  Q, A, False, P & Q, x:A  B(x), x:A. B(x), P  Q, x:AB(x), Dec(P), P  Q, left + right, s = t
Lemmas	cons before, l before wf, decidable or, l member wf, decidable cand